Report for CWE789-1/CWE789_Uncontrolled_Mem_Alloc---s01---CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad.i

Generated on 2025-03-01 23:14:41 by CPAchecker 4.0

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
Name Value
1
// This file is part of the SV-Benchmarks collection of verification tasks:  
2
// https://github.com/sosy-lab/sv-benchmarks  
3
//  
4
// SPDX-FileCopyrightText: 2010-2020 NIST  
5
// SPDX-FileCopyrightText: 2020 The SV-Benchmarks Community  
6
//  
7
// SPDX-License-Identifier: CC0-1.0  
8
  
9
/* Generated by Frama-C */  
10
  
11
typedef unsigned long size_t;  
12
  
13
typedef int wchar_t;  
14
  
15
typedef long __int64_t;  
16
  
17
typedef __int64_t int64_t;  
18
  
19
typedef unsigned int wint_t;  
20
  
21
struct _twoIntsStruct {  
22
   int intOne ;  
23
   int intTwo ;  
24
};  
25
  
26
typedef struct _twoIntsStruct twoIntsStruct;  
27
  
28
struct __pthread_internal_list {  
29
   struct __pthread_internal_list *__prev ;  
30
   struct __pthread_internal_list *__next ;  
31
};  
32
  
33
typedef struct __pthread_internal_list __pthread_list_t;  
34
  
35
struct __pthread_mutex_s {  
36
   int __lock ;  
37
   unsigned int __count ;  
38
   int __owner ;  
39
   unsigned int __nusers ;  
40
   int __kind ;  
41
   short __spins ;  
42
   short __elision ;  
43
   __pthread_list_t __list ;  
44
};  
45
  
46
typedef unsigned long pthread_t;  
47
  
48
union __anonunion_pthread_mutexattr_t_36 {  
49
   char __size[4U] ;  
50
   int __align ;  
51
};  
52
  
53
typedef union __anonunion_pthread_mutexattr_t_36 pthread_mutexattr_t;  
54
  
55
union pthread_attr_t {  
56
   char __size[56U] ;  
57
   long __align ;  
58
};  
59
  
60
typedef union pthread_attr_t pthread_attr_t;  
61
  
62
union __anonunion_pthread_mutex_t_38 {  
63
   struct __pthread_mutex_s __data ;  
64
   char __size[40U] ;  
65
   long __align ;  
66
};  
67
  
68
typedef union __anonunion_pthread_mutex_t_38 pthread_mutex_t;  
69
  
70
struct _stdThread;  
71
  
72
typedef struct _stdThread *stdThread;  
73
  
74
struct _stdThreadLock;  
75
  
76
typedef struct _stdThreadLock *stdThreadLock;  
77
  
78
struct _stdThread {  
79
   pthread_t handle ;  
80
   void (*start)(void *) ;  
81
   void *args ;  
82
};  
83
  
84
struct _stdThreadLock {  
85
   pthread_mutex_t mutex ;  
86
};  
87
  
88
typedef unsigned short __uint16_t;  
89
  
90
typedef unsigned int __uint32_t;  
91
  
92
typedef long __time_t;  
93
  
94
typedef long __ssize_t;  
95
  
96
typedef unsigned int __socklen_t;  
97
  
98
typedef __ssize_t ssize_t;  
99
  
100
typedef __time_t time_t;  
101
  
102
typedef __uint16_t uint16_t;  
103
  
104
typedef __uint32_t uint32_t;  
105
  
106
typedef __socklen_t socklen_t;  
107
  
108
typedef unsigned short sa_family_t;  
109
  
110
struct sockaddr {  
111
   sa_family_t sa_family ;  
112
   char sa_data[14U] ;  
113
};  
114
  
115
typedef uint32_t in_addr_t;  
116
  
117
struct in_addr {  
118
   in_addr_t s_addr ;  
119
};  
120
  
121
typedef uint16_t in_port_t;  
122
  
123
struct sockaddr_in {  
124
   sa_family_t sin_family ;  
125
   in_port_t sin_port ;  
126
   struct in_addr sin_addr ;  
127
   unsigned char sin_zero[8U] ;  
128
};  
129
  
130
int printf(char const * , ...);  
131
  
132
  
133
int sscanf(char const *, char const * , ...);  
134
  
135
  
136
int puts(char const *);  
137
  
138
  
139
int rand(void);  
140
  
141
  
142
int iswxdigit(wint_t);  
143
  
144
  
145
unsigned short const **__ctype_b_loc(void);  
146
  
147
  
148
int const GLOBAL_CONST_TRUE;  
149
  
150
  
151
int const GLOBAL_CONST_FALSE;  
152
  
153
  
154
int const GLOBAL_CONST_FIVE;  
155
  
156
  
157
int globalTrue;  
158
  
159
  
160
int globalFalse;  
161
  
162
  
163
int globalFive;  
164
  
165
  
166
void printLine(char const *line);  
167
  
168
  
169
void printWLine(wchar_t const *line);  
170
  
171
  
172
void printIntLine(int intNumber);  
173
  
174
  
175
void printShortLine(short shortNumber);  
176
  
177
  
178
void printFloatLine(float floatNumber);  
179
  
180
  
181
void printLongLine(long longNumber);  
182
  
183
  
184
void printLongLongLine(int64_t longLongIntNumber);  
185
  
186
  
187
void printSizeTLine(size_t sizeTNumber);  
188
  
189
  
190
void printHexCharLine(char charHex);  
191
  
192
  
193
void printWcharLine(wchar_t wideChar);  
194
  
195
  
196
void printUnsignedLine(unsigned int unsignedNumber);  
197
  
198
  
199
void printHexUnsignedCharLine(unsigned char unsignedCharacter);  
200
  
201
  
202
void printDoubleLine(double doubleNumber);  
203
  
204
  
205
void printStructLine(twoIntsStruct const *structTwoIntsStruct);  
206
  
207
  
208
void printBytesLine(unsigned char const *bytes, size_t numBytes);  
209
  
210
  
211
size_t decodeHexChars(unsigned char *bytes, size_t numBytes, char const *hex);  
212
  
213
  
214
size_t decodeHexWChars(unsigned char *bytes, size_t numBytes, wchar_t const *hex);  
215
  
216
  
217
int globalReturnsTrue(void);  
218
  
219
  
220
int globalReturnsFalse(void);  
221
  
222
  
223
int globalReturnsTrueOrFalse(void);  
224
  
225
  
226
int globalArgc;  
227
  
228
  
229
char **globalArgv;  
230
  
231
  
232
int wprintf(wchar_t const * , ...);  
233
  
234
  
235
int swscanf(wchar_t const *, wchar_t const * , ...);  
236
  
237
  
238
void printLine(char const *line)  
239
{  
240
    
241
  if (line != (char const *)0)   
242
                               printf("%s\n",line); else ;  
243
    
244
  return;  
245
}  
246
  
247
  
248
void printWLine(wchar_t const *line)  
249
{  
250
    
251
  if (line != (wchar_t const *)0)   
252
                                  wprintf((wchar_t const *)L"%" "l" "s" "\\n" ,line); else ;  
253
    
254
  return;  
255
}  
256
  
257
  
258
void printIntLine(int intNumber)  
259
{  
260
    
261
  printf("%d\n",intNumber);  
262
    
263
  return;  
264
}  
265
  
266
  
267
  
268
  
269
void printFloatLine(float floatNumber)  
270
{  
271
    
272
  printf("%f\n",(double)floatNumber);  
273
    
274
  return;  
275
}  
276
  
277
  
278
void printLongLine(long longNumber)  
279
{  
280
    
281
  printf("%ld\n",longNumber);  
282
    
283
  return;  
284
}  
285
  
286
  
287
  
288
  
289
void printSizeTLine(size_t sizeTNumber)  
290
{  
291
    
292
  printf("%zu\n",sizeTNumber);  
293
    
294
  return;  
295
}  
296
  
297
  
298
void printHexCharLine(char charHex)  
299
{  
300
    
301
  printf("%02x\n",(int)charHex);  
302
    
303
  return;  
304
}  
305
  
306
  
307
void printWcharLine(wchar_t wideChar)  
308
{  
309
  wchar_t s[2U];  
310
    
311
  s[0] = wideChar;  
312
    
313
  s[1] = 0;  
314
    
315
  printf("%ls\n",(wchar_t *)(& s));  
316
    
317
  return;  
318
}  
319
  
320
  
321
void printUnsignedLine(unsigned int unsignedNumber)  
322
{  
323
    
324
  printf("%u\n",unsignedNumber);  
325
    
326
  return;  
327
}  
328
  
329
  
330
void printHexUnsignedCharLine(unsigned char unsignedCharacter)  
331
{  
332
    
333
  printf("%02x\n",(int)unsignedCharacter);  
334
    
335
  return;  
336
}  
337
  
338
  
339
void printDoubleLine(double doubleNumber)  
340
{  
341
    
342
  printf("%g\n",doubleNumber);  
343
    
344
  return;  
345
}  
346
  
347
  
348
void printStructLine(twoIntsStruct const *structTwoIntsStruct)  
349
{  
350
    
351
  printf("%d -- %d\n",structTwoIntsStruct->intOne,structTwoIntsStruct->intTwo);  
352
    
353
  return;  
354
}  
355
  
356
  
357
void printBytesLine(unsigned char const *bytes, size_t numBytes)  
358
{  
359
  size_t i;  
360
    
361
  i = 0UL;  
362
    
363
  goto ldv_3392;  
364
  ldv_3391:   
365
  ;  
366
    
367
  printf("%02x",(int)*(bytes + i));  
368
    
369
  i += 1UL;  
370
  ldv_3392:   
371
  ;  
372
    
373
  if (i < numBytes)   
374
                    goto ldv_3391; else   
375
                                        goto ldv_3393;  
376
  ldv_3393:   
377
  ;  
378
    
379
  puts("");  
380
    
381
  return;  
382
}  
383
  
384
  
385
size_t decodeHexChars(unsigned char *bytes, size_t numBytes, char const *hex)  
386
{  
387
    
388
  size_t numWritten = 0UL;  
389
    
390
  goto ldv_3402;  
391
  ldv_3401:   
392
  ;  
393
  {  
394
    int byte;  
395
      
396
    sscanf(hex + numWritten * 2UL,"%02x",& byte);  
397
      
398
    *(bytes + numWritten) = (unsigned char)byte;  
399
      
400
    numWritten += 1UL;  
401
  }  
402
  ldv_3402:   
403
  ;  
404
    
405
  if (numWritten < numBytes) {  
406
    unsigned short const **tmp;  
407
      
408
    tmp = __ctype_b_loc();  
409
      
410
    ;  
411
      
412
    if (((int)*(*tmp + (int)*(hex + numWritten * 2UL)) & 4096) != 0) {  
413
      unsigned short const **tmp_0;  
414
        
415
      tmp_0 = __ctype_b_loc();  
416
        
417
      ;  
418
        
419
      if (((int)*(*tmp_0 + (int)*(hex + (numWritten * 2UL + (size_t)1U))) & 4096) != 0)   
420
          
421
        goto ldv_3401; else   
422
                            goto ldv_3403;  
423
    }  
424
    else   
425
         goto ldv_3403;  
426
  }  
427
  else   
428
       goto ldv_3403;  
429
  ldv_3403:   
430
  ;  
431
    
432
  return numWritten;  
433
}  
434
  
435
  
436
size_t decodeHexWChars(unsigned char *bytes, size_t numBytes, wchar_t const *hex)  
437
{  
438
    
439
  size_t numWritten = 0UL;  
440
    
441
  goto ldv_3412;  
442
  ldv_3411:   
443
  ;  
444
  {  
445
    int byte;  
446
      
447
    swscanf(hex + numWritten * 2UL,(wchar_t const *)L"%" "0" "2" "x" ,& byte);  
448
      
449
    *(bytes + numWritten) = (unsigned char)byte;  
450
      
451
    numWritten += 1UL;  
452
  }  
453
  ldv_3412:   
454
  ;  
455
    
456
  if (numWritten < numBytes) {  
457
    int tmp;  
458
      
459
    tmp = iswxdigit((unsigned int)*(hex + numWritten * 2UL));  
460
      
461
    if (tmp != 0) {  
462
      int tmp_0;  
463
        
464
      tmp_0 = iswxdigit((unsigned int)*(hex + (numWritten * 2UL + (size_t)1U)));  
465
        
466
      if (tmp_0 != 0)   
467
                      goto ldv_3411; else   
468
                                          goto ldv_3413;  
469
    }  
470
    else   
471
         goto ldv_3413;  
472
  }  
473
  else   
474
       goto ldv_3413;  
475
  ldv_3413:   
476
  ;  
477
    
478
  return numWritten;  
479
}  
480
  
481
  
482
int globalReturnsTrue(void)  
483
{  
484
  int __retres;  
485
    
486
  __retres = 1;  
487
    
488
  return __retres;  
489
}  
490
  
491
  
492
int globalReturnsFalse(void)  
493
{  
494
  int __retres;  
495
    
496
  __retres = 0;  
497
    
498
  return __retres;  
499
}  
500
  
501
  
502
int globalReturnsTrueOrFalse(void)  
503
{  
504
  int __retres;  
505
  int tmp;  
506
    
507
  tmp = rand();  
508
    
509
  __retres = tmp % 2;  
510
    
511
  return __retres;  
512
}  
513
  
514
  
515
int const GLOBAL_CONST_TRUE = 1;  
516
  
517
int const GLOBAL_CONST_FALSE = 0;  
518
  
519
int const GLOBAL_CONST_FIVE = 5;  
520
  
521
int globalTrue = 1;  
522
  
523
int globalFalse = 0;  
524
  
525
int globalFive = 5;  
526
  
527
void good1(void)  
528
{  
529
    
530
  return;  
531
}  
532
  
533
  
534
void good2(void)  
535
{  
536
    
537
  return;  
538
}  
539
  
540
  
541
void good3(void)  
542
{  
543
    
544
  return;  
545
}  
546
  
547
  
548
void good4(void)  
549
{  
550
    
551
  return;  
552
}  
553
  
554
  
555
void good5(void)  
556
{  
557
    
558
  return;  
559
}  
560
  
561
  
562
void good6(void)  
563
{  
564
    
565
  return;  
566
}  
567
  
568
  
569
void good7(void)  
570
{  
571
    
572
  return;  
573
}  
574
  
575
  
576
void good8(void)  
577
{  
578
    
579
  return;  
580
}  
581
  
582
  
583
void good9(void)  
584
{  
585
    
586
  return;  
587
}  
588
  
589
  
590
void bad1(void)  
591
{  
592
    
593
  return;  
594
}  
595
  
596
  
597
void bad2(void)  
598
{  
599
    
600
  return;  
601
}  
602
  
603
  
604
void bad3(void)  
605
{  
606
    
607
  return;  
608
}  
609
  
610
  
611
void bad4(void)  
612
{  
613
    
614
  return;  
615
}  
616
  
617
  
618
void bad5(void)  
619
{  
620
    
621
  return;  
622
}  
623
  
624
  
625
void bad6(void)  
626
{  
627
    
628
  return;  
629
}  
630
  
631
  
632
void bad7(void)  
633
{  
634
    
635
  return;  
636
}  
637
  
638
  
639
void bad8(void)  
640
{  
641
    
642
  return;  
643
}  
644
  
645
  
646
void bad9(void)  
647
{  
648
    
649
  return;  
650
}  
651
  
652
  
653
int globalArgc = 0;  
654
  
655
char **globalArgv = (char **)0;  
656
  
657
void *malloc(size_t);  
658
  
659
  
660
void free(void *);  
661
  
662
  
663
int pthread_create(pthread_t *, pthread_attr_t const *, void *(*)(void *), void *);  
664
  
665
  
666
void pthread_exit(void *);  
667
  
668
  
669
int pthread_join(pthread_t, void **);  
670
  
671
  
672
int pthread_mutex_init(pthread_mutex_t *, pthread_mutexattr_t const *);  
673
  
674
  
675
int pthread_mutex_destroy(pthread_mutex_t *);  
676
  
677
  
678
int pthread_mutex_lock(pthread_mutex_t *);  
679
  
680
  
681
int pthread_mutex_unlock(pthread_mutex_t *);  
682
  
683
  
684
int stdThreadCreate(void (*start)(void *), void *args, stdThread *thread);  
685
  
686
  
687
int stdThreadJoin(stdThread thread);  
688
  
689
  
690
int stdThreadDestroy(stdThread thread);  
691
  
692
  
693
int stdThreadLockCreate(stdThreadLock *lock);  
694
  
695
  
696
void stdThreadLockAcquire(stdThreadLock lock);  
697
  
698
  
699
void stdThreadLockRelease(stdThreadLock lock);  
700
  
701
  
702
void stdThreadLockDestroy(stdThreadLock lock);  
703
  
704
  
705
static void *internal_start(void *args)  
706
{  
707
  void *__retres;  
708
    
709
  stdThread thread = (struct _stdThread *)args;  
710
    
711
  (*(thread->start))(thread->args);  
712
    
713
  pthread_exit((void *)0);  
714
    
715
  __retres = (void *)0;  
716
    
717
  return __retres;  
718
}  
719
  
720
  
721
int stdThreadCreate(void (*start)(void *), void *args, stdThread *thread)  
722
{  
723
  int __retres;  
724
  pthread_t handle;  
725
  stdThread my_thread;  
726
  int tmp_0;  
727
    
728
  *thread = (struct _stdThread *)0;  
729
    
730
  my_thread = (stdThread)malloc(24UL);  
731
    
732
  if (my_thread == (struct _stdThread *)0) {  
733
      
734
    __retres = 0;  
735
      
736
    goto return_label;  
737
  }  
738
  else ;  
739
    
740
  my_thread->start = start;  
741
    
742
  my_thread->args = args;  
743
    
744
  tmp_0 = pthread_create(& handle,(pthread_attr_t const *)0,& internal_start,(void *)my_thread);  
745
    
746
  if (tmp_0 != 0) {  
747
      
748
    free((void *)my_thread);  
749
      
750
    __retres = 0;  
751
      
752
    goto return_label;  
753
  }  
754
  else ;  
755
    
756
  my_thread->handle = handle;  
757
    
758
  *thread = my_thread;  
759
    
760
  __retres = 1;  
761
  return_label:   
762
                return __retres;  
763
}  
764
  
765
  
766
int stdThreadJoin(stdThread thread)  
767
{  
768
  int __retres;  
769
  void *dummy;  
770
  int tmp;  
771
    
772
  tmp = pthread_join(thread->handle,& dummy);  
773
    
774
  if (tmp != 0) {  
775
      
776
    __retres = 0;  
777
      
778
    goto return_label;  
779
  }  
780
  else ;  
781
    
782
  __retres = 1;  
783
  return_label:   
784
                return __retres;  
785
}  
786
  
787
  
788
int stdThreadDestroy(stdThread thread)  
789
{  
790
  int __retres;  
791
    
792
  free((void *)thread);  
793
    
794
  __retres = 1;  
795
    
796
  return __retres;  
797
}  
798
  
799
  
800
int stdThreadLockCreate(stdThreadLock *lock)  
801
{  
802
  int __retres;  
803
  int tmp_0;  
804
    
805
  stdThreadLock my_lock = (struct _stdThreadLock *)0;  
806
    
807
  *lock = (struct _stdThreadLock *)0;  
808
    
809
  my_lock = (stdThreadLock)malloc(40UL);  
810
    
811
  if (my_lock == (struct _stdThreadLock *)0) {  
812
      
813
    __retres = 0;  
814
      
815
    goto return_label;  
816
  }  
817
  else ;  
818
    
819
  tmp_0 = pthread_mutex_init(& my_lock->mutex,(pthread_mutexattr_t const *)0);  
820
    
821
  if (tmp_0 != 0) {  
822
      
823
    free((void *)lock);  
824
      
825
    __retres = 0;  
826
      
827
    goto return_label;  
828
  }  
829
  else ;  
830
    
831
  *lock = my_lock;  
832
    
833
  __retres = 1;  
834
  return_label:   
835
                return __retres;  
836
}  
837
  
838
  
839
void stdThreadLockAcquire(stdThreadLock lock)  
840
{  
841
    
842
  pthread_mutex_lock(& lock->mutex);  
843
    
844
  return;  
845
}  
846
  
847
  
848
void stdThreadLockRelease(stdThreadLock lock)  
849
{  
850
    
851
  pthread_mutex_unlock(& lock->mutex);  
852
    
853
  return;  
854
}  
855
  
856
  
857
void stdThreadLockDestroy(stdThreadLock lock)  
858
{  
859
    
860
  pthread_mutex_destroy(& lock->mutex);  
861
    
862
  free((void *)lock);  
863
    
864
  return;  
865
}  
866
  
867
  
868
void ldv_exit(void);  
869
  
870
  
871
char *ldv_strcpy(char *dest, char const *src);  
872
  
873
  
874
size_t ldv_strlen(char const *str);  
875
  
876
  
877
unsigned long strtoul(char const *, char **, int);  
878
  
879
  
880
void srand(unsigned int);  
881
  
882
  
883
static void ldv_exit_2(int ldv_func_arg1);  
884
  
885
  
886
time_t time(time_t *);  
887
  
888
  
889
void *memset(void *, int, size_t);  
890
  
891
  
892
static char *ldv_strcpy_3(char * __restrict ldv_func_arg1, char const * __restrict ldv_func_arg2);  
893
  
894
  
895
static size_t ldv_strlen_1(char const *ldv_func_arg1);  
896
  
897
  
898
int socket(int, int, int);  
899
  
900
  
901
int connect(int, struct sockaddr const *, socklen_t);  
902
  
903
  
904
ssize_t recv(int, void *, size_t, int);  
905
  
906
  
907
uint16_t htons(uint16_t);  
908
  
909
  
910
in_addr_t inet_addr(char const *);  
911
  
912
  
913
int close(int);  
914
  
915
  
916
void CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad(void)  
917
{  
918
  size_t data;  
919
    
920
  data = 0UL;  
921
  {  
922
    int recvResult;  
923
    struct sockaddr_in service;  
924
    char inputBuffer[26U];  
925
    int tmp;  
926
    ssize_t tmp_0;  
927
      
928
    int connectSocket = -1;  
929
      
930
    connectSocket = socket(2,1,6);  
931
      
932
    if (connectSocket == -1)   
933
                             goto ldv_4160; else ;  
934
      
935
    memset((void *)(& service),0,16UL);  
936
      
937
    service.sin_family = (unsigned short)2U;  
938
      
939
    service.sin_addr.s_addr = inet_addr("127.0.0.1");  
940
      
941
    service.sin_port = htons((unsigned short)27015);  
942
      
943
    tmp = connect(connectSocket,(struct sockaddr const *)(& service),16U);  
944
      
945
    if (tmp == -1)   
946
                   goto ldv_4160; else ;  
947
      
948
    tmp_0 = recv(connectSocket,(void *)(& inputBuffer),25UL,0);  
949
      
950
    recvResult = (int)tmp_0;  
951
      
952
    if (recvResult == -1 || recvResult == 0)   
953
                                             goto ldv_4160; else ;  
954
      
955
    inputBuffer[recvResult] = (char)0;  
956
      
957
    data = strtoul((char const *)(& inputBuffer),(char **)0,0);  
958
    ldv_4160:   
959
    ;  
960
      
961
    if (connectSocket != -1)   
962
                             close(connectSocket); else ;  
963
  }  
964
  {  
965
    char *myString;  
966
    size_t tmp_2;  
967
      
968
    tmp_2 = ldv_strlen_1("hello");  
969
      
970
    ;  
971
      
972
    if (tmp_2 < data) {  
973
        
974
      myString = (char *)malloc(data);  
975
        
976
      if (myString == (char *)0)   
977
                                 ldv_exit_2(-1); else ;  
978
        
979
      ldv_strcpy_3(myString,"hello");  
980
        
981
      printLine((char const *)myString);  
982
        
983
      free((void *)myString);  
984
    }  
985
    else   
986
         printLine("Input is less than the length of the source string");  
987
  }  
988
    
989
  return;  
990
}  
991
  
992
  
993
int main(int argc, char **argv)  
994
{  
995
  int __retres;  
996
  {  
997
    time_t tmp;  
998
      
999
    tmp = time((time_t *)0L);  
1000
      
1001
    srand((unsigned int)tmp);  
1002
      
1003
    printLine("Calling bad()...");  
1004
      
1005
    CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad();  
1006
      
1007
    printLine("Finished bad()");  
1008
      
1009
    __retres = 0;  
1010
      
1011
    goto return_label;  
1012
  }  
1013
    
1014
  __retres = 0;  
1015
  return_label:   
1016
                return __retres;  
1017
}  
1018
  
1019
  
1020
static size_t ldv_strlen_1(char const *ldv_func_arg1)  
1021
{  
1022
  size_t tmp;  
1023
    
1024
  tmp = ldv_strlen(ldv_func_arg1);  
1025
    
1026
  return tmp;  
1027
}  
1028
  
1029
  
1030
static void ldv_exit_2(int ldv_func_arg1)  
1031
{  
1032
    
1033
  ldv_exit();  
1034
    
1035
  return;  
1036
}  
1037
  
1038
  
1039
static char *ldv_strcpy_3(char * __restrict ldv_func_arg1, char const * __restrict ldv_func_arg2)  
1040
{  
1041
  char *tmp;  
1042
    
1043
  tmp = ldv_strcpy(ldv_func_arg1,ldv_func_arg2);  
1044
    
1045
  return tmp;  
1046
}  
1047
  
1048
  
1049
void *ldv_xmalloc(size_t size);  
1050
  
1051
  
1052
int ldv_undef_int(void);  
1053
  
1054
  
1055
int ldv_undef_int_positive(void);  
1056
  
1057
  
1058
int ldv_asprintf(char **ptr);  
1059
  
1060
  
1061
int ldv_asprintf(char **ptr)  
1062
{  
1063
  int __retres;  
1064
  char *new;  
1065
  int tmp_1;  
1066
    
1067
  tmp_1 = ldv_undef_int();  
1068
    
1069
  if (tmp_1 != 0) {  
1070
    int tmp_0;  
1071
      
1072
    new = (char *)ldv_xmalloc(1UL);  
1073
      
1074
    *ptr = new;  
1075
      
1076
    tmp_0 = ldv_undef_int_positive();  
1077
      
1078
    __retres = tmp_0;  
1079
      
1080
    goto return_label;  
1081
  }  
1082
  else {  
1083
      
1084
    __retres = -1;  
1085
      
1086
    goto return_label;  
1087
  }  
1088
  return_label:   
1089
                return __retres;  
1090
}  
1091
  
1092
  
1093
void abort(void);  
1094
void assume_abort_if_not(int cond) {  
1095
  if(!cond) {abort();}  
1096
}  
1097
  
1098
  
1099
void ldv_exit(void)  
1100
{  
1101
    
1102
  assume_abort_if_not(0);  
1103
    
1104
  return;  
1105
}  
1106
  
1107
  
1108
void *ldv_xmalloc(size_t size);  
1109
  
1110
  
1111
void *memcpy(void *, void const *, size_t);  
1112
  
1113
  
1114
char *ldv_strdup(char const *s);  
1115
  
1116
  
1117
char *ldv_strncpy(char *dest, char const *src, size_t n);  
1118
  
1119
  
1120
char *ldv_strdup(char const *s)  
1121
{  
1122
  char *__retres;  
1123
  char *new;  
1124
  int tmp_2;  
1125
    
1126
  tmp_2 = ldv_undef_int();  
1127
    
1128
  if (tmp_2 != 0) {  
1129
    void *tmp_0;  
1130
    size_t tmp;  
1131
    size_t tmp_1;  
1132
      
1133
    tmp = ldv_strlen(s);  
1134
      
1135
    tmp_0 = ldv_xmalloc(tmp);  
1136
      
1137
    new = (char *)tmp_0;  
1138
      
1139
    tmp_1 = ldv_strlen(s);  
1140
      
1141
    ;  
1142
      
1143
    ;  
1144
      
1145
    memcpy((void *)new,(void const *)s,tmp_1);  
1146
      
1147
    __retres = new;  
1148
      
1149
    goto return_label;  
1150
  }  
1151
  else {  
1152
      
1153
    __retres = (char *)0;  
1154
      
1155
    goto return_label;  
1156
  }  
1157
  return_label:   
1158
                return __retres;  
1159
}  
1160
  
1161
  
1162
size_t ldv_strlen(char const *str)  
1163
{  
1164
  size_t __retres;  
1165
  char const *s;  
1166
    
1167
  s = str;  
1168
    
1169
  goto ldv_1424;  
1170
  ldv_1423:   
1171
  ;  
1172
    
1173
  s += 1;  
1174
  ldv_1424:   
1175
  ;  
1176
    
1177
  if ((int)*s != 0)   
1178
                    goto ldv_1423; else   
1179
                                        goto ldv_1425;  
1180
  ldv_1425:   
1181
  ;  
1182
    
1183
  __retres = (unsigned long)((long)s - (long)str);  
1184
    
1185
  return __retres;  
1186
}  
1187
  
1188
  
1189
char *ldv_strncpy(char *dest, char const *src, size_t n)  
1190
{  
1191
  size_t i;  
1192
    
1193
  i = 0UL;  
1194
    
1195
  goto ldv_1433;  
1196
  ldv_1432:   
1197
  ;  
1198
    
1199
  *(dest + i) = *(src + i);  
1200
    
1201
  i += 1UL;  
1202
  ldv_1433:   
1203
  ;  
1204
    
1205
  if (i < n && (int)*(src + i) != 0)   
1206
                                     goto ldv_1432; else   
1207
                                                         goto ldv_1434;  
1208
  ldv_1434:   
1209
  ;  
1210
    
1211
  goto ldv_1436;  
1212
  ldv_1435:   
1213
  ;  
1214
    
1215
  *(dest + i) = (char)0;  
1216
    
1217
  i += 1UL;  
1218
  ldv_1436:   
1219
  ;  
1220
    
1221
  if (i < n)   
1222
             goto ldv_1435; else   
1223
                                 goto ldv_1437;  
1224
  ldv_1437:   
1225
  ;  
1226
    
1227
  return dest;  
1228
}  
1229
  
1230
  
1231
char *ldv_strcpy(char *dest, char const *src)  
1232
{  
1233
  size_t tmp;  
1234
    
1235
  tmp = ldv_strlen(src);  
1236
    
1237
  ;  
1238
    
1239
  ;  
1240
    
1241
  memcpy((void *)dest,(void const *)src,tmp);  
1242
    
1243
  return dest;  
1244
}  
1245
  
1246
  
1247
void *ldv_malloc(size_t size);  
1248
  
1249
  
1250
void *ldv_calloc(size_t nmemb, size_t size);  
1251
  
1252
  
1253
void *ldv_zalloc(size_t size);  
1254
  
1255
  
1256
void ldv_free(void *s);  
1257
  
1258
  
1259
void *ldv_realloc(void *ptr, size_t size);  
1260
  
1261
  
1262
void *ldv_xzalloc(size_t size);  
1263
  
1264
  
1265
  
1266
  
1267
  
1268
  
1269
  
1270
  
1271
void *ldv_reference_malloc(size_t size);  
1272
  
1273
  
1274
void *ldv_reference_calloc(size_t nmemb, size_t size);  
1275
  
1276
  
1277
void *ldv_reference_zalloc(size_t size);  
1278
  
1279
  
1280
void ldv_reference_free(void *s);  
1281
  
1282
  
1283
void *ldv_reference_realloc(void *ptr, size_t size);  
1284
  
1285
  
1286
void *ldv_reference_xmalloc(size_t size);  
1287
  
1288
  
1289
void *ldv_reference_xzalloc(size_t size);  
1290
  
1291
  
1292
  
1293
  
1294
  
1295
  
1296
  
1297
  
1298
  
1299
  
1300
void *ldv_malloc(size_t size)  
1301
{  
1302
  void *tmp;  
1303
    
1304
  tmp = ldv_reference_malloc(size);  
1305
    
1306
  return tmp;  
1307
}  
1308
  
1309
  
1310
void *ldv_calloc(size_t nmemb, size_t size)  
1311
{  
1312
  void *tmp;  
1313
    
1314
  tmp = ldv_reference_calloc(nmemb,size);  
1315
    
1316
  return tmp;  
1317
}  
1318
  
1319
  
1320
void *ldv_zalloc(size_t size)  
1321
{  
1322
  void *tmp;  
1323
    
1324
  tmp = ldv_reference_zalloc(size);  
1325
    
1326
  return tmp;  
1327
}  
1328
  
1329
  
1330
void ldv_free(void *s)  
1331
{  
1332
    
1333
  ldv_reference_free(s);  
1334
    
1335
  return;  
1336
}  
1337
  
1338
  
1339
void *ldv_xmalloc(size_t size)  
1340
{  
1341
  void *tmp;  
1342
    
1343
  tmp = ldv_reference_xmalloc(size);  
1344
    
1345
  return tmp;  
1346
}  
1347
  
1348
  
1349
void *ldv_xzalloc(size_t size)  
1350
{  
1351
  void *tmp;  
1352
    
1353
  tmp = ldv_reference_xzalloc(size);  
1354
    
1355
  return tmp;  
1356
}  
1357
  
1358
  
1359
  
1360
  
1361
  
1362
  
1363
  
1364
  
1365
  
1366
  
1367
void *ldv_realloc(void *ptr, size_t size)  
1368
{  
1369
  void *tmp;  
1370
    
1371
  tmp = ldv_reference_realloc(ptr,size);  
1372
    
1373
  return tmp;  
1374
}  
1375
  
1376
  
1377
void abort(void);  
1378
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
1379
void reach_error() { __assert_fail("0", "CWE789_Uncontrolled_Mem_Alloc---s01---CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad.i", 1371, "reach_error"); }  
1380
  
1381
  
1382
void ldv_error(void);  
1383
  
1384
  
1385
void ldv_error(void)  
1386
{  
1387
    
1388
  {reach_error();}  
1389
    
1390
  return;  
1391
}  
1392
  
1393
  
1394
  
1395
  
1396
  
1397
int ldv_undef_long(void);  
1398
  
1399
  
1400
unsigned int ldv_undef_uint(void);  
1401
  
1402
  
1403
unsigned long ldv_undef_ulong(void);  
1404
  
1405
  
1406
unsigned long long ldv_undef_ulonglong(void);  
1407
  
1408
  
1409
  
1410
  
1411
int ldv_undef_int_negative(void);  
1412
  
1413
  
1414
int ldv_undef_int_nonpositive(void);  
1415
  
1416
  
1417
  
1418
  
1419
int __VERIFIER_nondet_int(void);  
1420
  
1421
  
1422
long __VERIFIER_nondet_long(void);  
1423
  
1424
  
1425
unsigned int __VERIFIER_nondet_uint(void);  
1426
  
1427
  
1428
unsigned long __VERIFIER_nondet_ulong(void);  
1429
  
1430
  
1431
unsigned long long __VERIFIER_nondet_ulonglong(void);  
1432
  
1433
  
1434
  
1435
  
1436
int ldv_undef_int(void)  
1437
{  
1438
  int tmp;  
1439
    
1440
  tmp = __VERIFIER_nondet_int();  
1441
    
1442
  return tmp;  
1443
}  
1444
  
1445
  
1446
int ldv_undef_long(void)  
1447
{  
1448
  int __retres;  
1449
  long tmp;  
1450
    
1451
  tmp = __VERIFIER_nondet_long();  
1452
    
1453
  __retres = (int)tmp;  
1454
    
1455
  return __retres;  
1456
}  
1457
  
1458
  
1459
unsigned int ldv_undef_uint(void)  
1460
{  
1461
  unsigned int tmp;  
1462
    
1463
  tmp = __VERIFIER_nondet_uint();  
1464
    
1465
  return tmp;  
1466
}  
1467
  
1468
  
1469
  
1470
  
1471
unsigned long ldv_undef_ulong(void)  
1472
{  
1473
  unsigned long tmp;  
1474
    
1475
  tmp = __VERIFIER_nondet_ulong();  
1476
    
1477
  return tmp;  
1478
}  
1479
  
1480
  
1481
unsigned long long ldv_undef_ulonglong(void)  
1482
{  
1483
  unsigned long long tmp;  
1484
    
1485
  tmp = __VERIFIER_nondet_ulonglong();  
1486
    
1487
  return tmp;  
1488
}  
1489
  
1490
  
1491
int ldv_undef_int_positive(void)  
1492
{  
1493
    
1494
  int ret = ldv_undef_int();  
1495
    
1496
  assume_abort_if_not(ret > 0);  
1497
    
1498
  return ret;  
1499
}  
1500
  
1501
  
1502
int ldv_undef_int_negative(void)  
1503
{  
1504
    
1505
  int ret = ldv_undef_int();  
1506
    
1507
  assume_abort_if_not(ret < 0);  
1508
    
1509
  return ret;  
1510
}  
1511
  
1512
  
1513
int ldv_undef_int_nonpositive(void)  
1514
{  
1515
    
1516
  int ret = ldv_undef_int();  
1517
    
1518
  assume_abort_if_not(ret <= 0);  
1519
    
1520
  return ret;  
1521
}  
1522
  
1523
  
1524
  
1525
  
1526
  
1527
  
1528
void *calloc(size_t, size_t);  
1529
  
1530
  
1531
void *ldv_reference_malloc(size_t size)  
1532
{  
1533
  void *__retres;  
1534
  void *res;  
1535
  int tmp;  
1536
    
1537
  tmp = ldv_undef_int();  
1538
    
1539
  if (tmp != 0) {  
1540
      
1541
    res = malloc(size);  
1542
      
1543
    assume_abort_if_not(res != (void *)0);  
1544
      
1545
    __retres = res;  
1546
      
1547
    goto return_label;  
1548
  }  
1549
  else {  
1550
      
1551
    __retres = (void *)0;  
1552
      
1553
    goto return_label;  
1554
  }  
1555
  return_label:   
1556
                return __retres;  
1557
}  
1558
  
1559
  
1560
void *ldv_reference_calloc(size_t nmemb, size_t size)  
1561
{  
1562
  void *tmp;  
1563
    
1564
  tmp = calloc(nmemb,size);  
1565
    
1566
  return tmp;  
1567
}  
1568
  
1569
  
1570
void *ldv_reference_zalloc(size_t size)  
1571
{  
1572
  void *tmp;  
1573
    
1574
  tmp = calloc(1UL,size);  
1575
    
1576
  return tmp;  
1577
}  
1578
  
1579
  
1580
void ldv_reference_free(void *s)  
1581
{  
1582
    
1583
  free(s);  
1584
    
1585
  return;  
1586
}  
1587
  
1588
  
1589
void *ldv_reference_realloc(void *ptr, size_t size)  
1590
{  
1591
  void *__retres;  
1592
  void *res;  
1593
  int tmp;  
1594
    
1595
  if (ptr != (void *)0 && size == 0UL) {  
1596
      
1597
    free(ptr);  
1598
      
1599
    __retres = (void *)0;  
1600
      
1601
    goto return_label;  
1602
  }  
1603
  else ;  
1604
    
1605
  if (ptr == (void *)0) {  
1606
      
1607
    res = malloc(size);  
1608
      
1609
    __retres = res;  
1610
      
1611
    goto return_label;  
1612
  }  
1613
  else ;  
1614
    
1615
  tmp = ldv_undef_int();  
1616
    
1617
  if (tmp != 0) {  
1618
      
1619
    res = malloc(size);  
1620
      
1621
    assume_abort_if_not(res != (void *)0);  
1622
      
1623
    memcpy(res,(void const *)ptr,size);  
1624
      
1625
    free(ptr);  
1626
      
1627
    __retres = res;  
1628
      
1629
    goto return_label;  
1630
  }  
1631
  else {  
1632
      
1633
    __retres = (void *)0;  
1634
      
1635
    goto return_label;  
1636
  }  
1637
  return_label:   
1638
                return __retres;  
1639
}  
1640
  
1641
  
1642
void *ldv_reference_xmalloc(size_t size)  
1643
{  
1644
  void *res;  
1645
    
1646
  res = malloc(size);  
1647
    
1648
  assume_abort_if_not(res != (void *)0);  
1649
    
1650
  return res;  
1651
}  
1652
  
1653
  
1654
void *ldv_reference_xzalloc(size_t size)  
1655
{  
1656
  void *res;  
1657
    
1658
  res = calloc(1UL,size);  
1659
    
1660
  assume_abort_if_not(res != (void *)0);  
1661
    
1662
  return res;  
1663
}  
1664
  
1665
  
1666
  
1667
  
1668
  
1669
  
1670
  
1671
  
1672
  
1673
  

Log not available

Statistics NameStatistics ValueAdditional Value
Parallel Algorithm statistics
Number of algorithms used 5
Successful analysis /opt/cpachecker/config/components/smgAnalysis-symEx.properties
Statistics for /opt/cpachecker/config/components/smgAnalysis-symEx.properties
==============================================================================
SMGCPA statistics
Number of variables per state 17.51 sum: 613, count: 35, min: 0, max: 25
Number of global variables per state 8.51 sum: 298, count: 35, min: 0, max: 10
Time for solving constraints 0.361s
Time for independent computation 0.010s
Time for SMT check 0.007s
Time for resolving definites 0.028s
Cache lookups 13
Direct cache hits 3
Direct cache lookup time 0.001s
Number of assumptions 20
Number of deterministic assumptions 0
Level of Determinism 0%
Number of list materializations : 0
Total time spent on materialization : 0ms
Max time spent on materialization : 0ms
Number of 0+ materializations 0
Total time spent on 0+ materialization : 0ms
Max time spent on 0+ materialization : 0ms
Number of lists abstracted in total : 0
Total time spent on list abstraction : 0ms
Max time spent on list abstraction : 0ms
Total time spent on searching for list abstractions : 0ms
Max time spent on searching a single list abstractions : 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states 1
Total time for successor computation 0.010s
Total time for strengthen operator 0.129s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions 0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states 1
Total time for successor computation 0.005s
Total time for strengthen operator 0.086s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions 0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states 1
Total time for successor computation 0.002s
Total time for strengthen operator 0.074s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions 0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states 1
Total time for successor computation 0.016s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 31
Max size of waitlist 5
Average size of waitlist 2
Number of computed successors 35
Max successors for one state 2
Number of times merged 0
Number of times stopped 1
Number of times breaked 1
Total time for CPA algorithm 1.256s Max: 1.256s
Time for choose from waitlist 0.001s
Time for precision adjustment 0.042s
Time for transfer relation 1.174s
Time for stop operator 0.037s
Time for adding to reached set 0.000s
Statistics for /opt/cpachecker/config/components/smgAnalysis-symEx-concrete-memory-access.properties
=====================================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgAnalysis-symEx-concrete-memory-access.properties 0.002s
SMGCPA statistics
Number of variables per state 15.55 sum: 342, count: 22, min: 0, max: 20
Number of global variables per state 8.14 sum: 179, count: 22, min: 0, max: 9
Time for solving constraints 0.285s
Time for independent computation 0.002s
Time for SMT check 0.006s
Time for resolving definites 0.046s
Cache lookups 9
Direct cache hits 1
Direct cache lookup time 0.000s
Number of assumptions 12
Number of deterministic assumptions 0
Level of Determinism 0%
Number of list materializations : 0
Total time spent on materialization : 0ms
Max time spent on materialization : 0ms
Number of 0+ materializations 0
Total time spent on 0+ materialization : 0ms
Max time spent on 0+ materialization : 0ms
Number of lists abstracted in total : 0
Total time spent on list abstraction : 0ms
Max time spent on list abstraction : 0ms
Total time spent on searching for list abstractions : 0ms
Max time spent on searching a single list abstractions : 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states 1
Total time for successor computation 0.029s
Total time for strengthen operator 0.146s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions 0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states 1
Total time for successor computation 0.010s
Total time for strengthen operator 0.116s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions 0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states 1
Total time for successor computation 0.004s
Total time for strengthen operator 0.139s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions 0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states 1
Total time for successor computation 0.008s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 18
Max size of waitlist 5
Average size of waitlist 1
Number of computed successors 21
Max successors for one state 2
Number of times merged 0
Number of times stopped 0
Number of times breaked 0
Total time for CPA algorithm 1.196s Max: 1.196s
Time for choose from waitlist 0.000s
Time for precision adjustment 0.072s
Time for transfer relation 1.113s
Time for stop operator 0.009s
Time for adding to reached set 0.000s
Statistics for /opt/cpachecker/config/components/smgValueAnalysis-abstract-concrete-values-with-cex.properties
===============================================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgValueAnalysis-abstract-concrete-values-with-cex.properties 0.429s
SMGCPA statistics
Number of variables per state 17.36 sum: 573, count: 33, min: 0, max: 25
Number of global variables per state 8.48 sum: 280, count: 33, min: 0, max: 10
Number of assumptions 16
Number of deterministic assumptions 0
Level of Determinism 0%
Number of list materializations : 0
Total time spent on materialization : 0ms
Max time spent on materialization : 0ms
Number of 0+ materializations 0
Total time spent on 0+ materialization : 0ms
Max time spent on 0+ materialization : 0ms
Number of lists abstracted in total : 0
Total time spent on list abstraction : 0ms
Max time spent on list abstraction : 0ms
Total time spent on searching for list abstractions : 0ms
Max time spent on searching a single list abstractions : 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states 1
Total time for successor computation 0.028s
Total time for strengthen operator 0.210s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions 0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states 1
Total time for successor computation 0.025s
Total time for strengthen operator 0.116s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions 0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states 1
Total time for successor computation 0.005s
Total time for strengthen operator 0.055s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions 0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states 1
Total time for successor computation 0.007s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 28
Max size of waitlist 5
Average size of waitlist 2
Number of computed successors 34
Max successors for one state 2
Number of times merged 0
Number of times stopped 2
Number of times breaked 1
Total time for CPA algorithm 0.913s Max: 0.913s
Time for choose from waitlist 0.000s
Time for precision adjustment 0.064s
Time for transfer relation 0.776s
Time for stop operator 0.057s
Time for adding to reached set 0.008s
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 0 0%
Time for counterexample checks 1.642s
Statistics for /opt/cpachecker/config/components/smgValueAnalysis-with-cex.properties
======================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgValueAnalysis-with-cex.properties 0.432s
SMGCPA statistics
Number of variables per state 19.05 sum: 819, count: 43, min: 0, max: 28
Number of global variables per state 8.74 sum: 376, count: 43, min: 0, max: 10
Number of assumptions 24
Number of deterministic assumptions 0
Level of Determinism 0%
Number of list materializations : 0
Total time spent on materialization : 0ms
Max time spent on materialization : 0ms
Number of 0+ materializations 0
Total time spent on 0+ materialization : 0ms
Max time spent on 0+ materialization : 0ms
Number of lists abstracted in total : 0
Total time spent on list abstraction : 0ms
Max time spent on list abstraction : 0ms
Total time spent on searching for list abstractions : 0ms
Max time spent on searching a single list abstractions : 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states 1
Total time for successor computation 0.024s
Total time for strengthen operator 0.192s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions 0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states 1
Total time for successor computation 0.003s
Total time for strengthen operator 0.169s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions 0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states 1
Total time for successor computation 0.011s
Total time for strengthen operator 0.082s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions 0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states 1
Total time for successor computation 0.004s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 38
Max size of waitlist 5
Average size of waitlist 2
Number of computed successors 44
Max successors for one state 2
Number of times merged 0
Number of times stopped 2
Number of times breaked 1
Total time for CPA algorithm 0.964s Max: 0.964s
Time for choose from waitlist 0.001s
Time for precision adjustment 0.070s
Time for transfer relation 0.787s
Time for stop operator 0.087s
Time for adding to reached set 0.003s
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 0 0%
Time for counterexample checks 1.583s
Statistics for /opt/cpachecker/config/components/smgAnalysis-symEx-overapproximating-with-cex.properties
=========================================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgAnalysis-symEx-overapproximating-with-cex.properties 0.304s
SMGCPA statistics
Number of variables per state 15.74 sum: 362, count: 23, min: 0, max: 20
Number of global variables per state 8.17 sum: 188, count: 23, min: 0, max: 9
Time for solving constraints 0.245s
Time for independent computation 0.009s
Time for SMT check 0.029s
Time for resolving definites 0.066s
Cache lookups 9
Direct cache hits 0
Direct cache lookup time 0.000s
Number of assumptions 12
Number of deterministic assumptions 0
Level of Determinism 0%
Number of list materializations : 0
Total time spent on materialization : 0ms
Max time spent on materialization : 0ms
Number of 0+ materializations 0
Total time spent on 0+ materialization : 0ms
Max time spent on 0+ materialization : 0ms
Number of lists abstracted in total : 0
Total time spent on list abstraction : 0ms
Max time spent on list abstraction : 0ms
Total time spent on searching for list abstractions : 0ms
Max time spent on searching a single list abstractions : 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states 1
Total time for successor computation 0.012s
Total time for strengthen operator 0.304s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions 0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states 1
Total time for successor computation 0.000s
Total time for strengthen operator 0.198s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions 0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states 1
Total time for successor computation 0.002s
Total time for strengthen operator 0.119s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions 0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states 1
Total time for successor computation 0.001s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 18
Max size of waitlist 5
Average size of waitlist 1
Number of computed successors 22
Max successors for one state 2
Number of times merged 0
Number of times stopped 0
Number of times breaked 1
Total time for CPA algorithm 1.275s Max: 1.275s
Time for choose from waitlist 0.001s
Time for precision adjustment 0.049s
Time for transfer relation 1.195s
Time for stop operator 0.014s
Time for adding to reached set 0.002s
Counterexample-Check Algorithm statistics
Number of counterexample checks 1
Number of infeasible paths 0 0%
Time for counterexample checks 1.272s
Other statistics
================
Code Coverage
Function coverage 0.050
Visited lines 134
Total lines 507
Line coverage 0.264
Visited conditions 11
Total conditions 66
Condition coverage 0.167
CPAchecker general statistics
Number of program locations 778
Number of CFA edges (per node) 765 count: 778, min: 0, max: 8, avg: 0.98
Number of relevant variables 111
Number of functions 80
Number of loops (and loop nodes) 6 sum: 52, min: 5, max: 14, avg: 8.67
Size of reached set 35
Number of reached locations 30 4%
Avg states per location 1
Max states per location 4 at node N378
Number of reached functions 4 5%
Number of partitions 30
Avg size of partitions 1
Max size of partitions 4 with key [N378 before line 961, Function CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad called from node N406, stack depth 2 [73fafd4], stack [main, CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad], 20]
Number of target states 1
Size of final wait list 4
Time for analysis setup 7.745s
Time for loading CPAs 2.632s
Time for loading parser 0.569s
Time for CFA construction 3.404s
Time for parsing file(s) 0.773s
Time for AST to CFA 0.970s
Time for CFA sanity check 0.148s
Time for post-processing 1.384s
Time for loop structure 0.039s
Time for AST structure 0.000s
Time for CFA export 2.156s
Time for function pointers resolving 0.021s
Function calls via function pointers 1 count: 1, min: 1, max: 1, avg: 1.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.416s
Time for collecting variables 0.250s
Time for solving dependencies 0.008s
Time for building hierarchy 0.000s
Time for building classification 0.095s
Time for exporting data 0.063s
Time for Analysis 2.661s
CPU time for analysis 7.500s
Time for analyzing result 0.002s
Total time for CPAchecker 10.409s
Total CPU time for CPAchecker 21.010s
Time for statistics 0.215s
Time for Garbage Collector 0.562s in 4 runs
Garbage Collector(s) used PS MarkSweep, PS Scavenge
Used heap memory 191MB ( 182 MiB) max; 98MB ( 94 MiB) avg; 211MB ( 201 MiB) peak
Used non-heap memory 54MB ( 52 MiB) max; 36MB ( 34 MiB) avg; 56MB ( 53 MiB) peak
Used in PS Old Gen pool 20MB ( 19 MiB) max; 9MB ( 8 MiB) avg; 20MB ( 19 MiB) peak
Allocated heap memory 1002MB ( 956 MiB) max; 1002MB ( 956 MiB) avg
Allocated non-heap memory 57MB ( 55 MiB) max; 38MB ( 37 MiB) avg
Total process virtual memory 5609MB ( 5350 MiB) max; 4716MB ( 4498 MiB) avg
#Configuration NameConfiguration Value
1analysis.entryFunction main
2analysis.programNames CWE789-1/CWE789_Uncontrolled_Mem_Alloc---s01---CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad.i
3analysis.useParallelAnalyses true
4cfa.findLiveVariables true
5cfa.simplifyCfa false
6counterexample.export.compressWitness false
7counterexample.export.graphml witness.graphml
8counterexample.export.yaml witness.yml
9cpa.arg.compressWitness false
10cpa.arg.yamlProofWitness witness.yml
11cpa.callstack.unsupportedFunctions pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow,_longjmp,longjmp,siglongjmp
12cpa.smg2.handleUnknownFunctions ASSUME_EXTERNAL_ALLOCATED
13language C
14limits.time.cpu 30
15parallelAlgorithm.configFiles smgAnalysis-symEx.properties, smgAnalysis-symEx-concrete-memory-access.properties, smgValueAnalysis-abstract-concrete-values-with-cex.properties, smgValueAnalysis-with-cex.properties, smgAnalysis-symEx-overapproximating-with-cex.properties
16specification properties/valid-memsafety.prp

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}